es:ES, L:(Id List). fischer(L)  (e', e:E. fEvent(e)  (e <loc e')  rank(e) < rank(e')) 

latex

Definitions

A c B, x:A. B(x), e<e'.P(e), inc-snd(p), inc-fst(p), let x = a in b(x), x < y, True, T, P  Q, "$x", Id, ff, tt, if b then t else f fi , @i(x:T), Y, rank(e), x. t(x), {T}, SQType(T), S  T, , P & Q, , t  T, (e <loc e'), P  Q, x:A. B(x), P  Q, False, A  B, t.2, t.1, A, xL. P(x), @e(xv), (x  l), b, e loc e' , P  Q, Unit, , x(s), WellFnd{i}(A;x,y.R(x;y)), fEvent(e), fischer(L),

Lemmas

es-locl-iff, es-loc-pred, es-when wf, assert-changed, pi2 wf, pi1 wf, not functionality wrt iff, assert-eq-id, es-after wf, eq id wf, nat wf, es-E wf, es-dtype wf, squash wf, loc-last-change, es-le-last-change, last-change-property, last-change wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, not wf, bnot wf, bool wf, es-vartype wf, es-isconst wf, assert wf, changed wf, es-locl wf, es-locl-wellfnd, Id sq, le wf, f-rank wf, intpair-less wf, es-causl wf, es-loc wf, f-event wf, event system wf, Id wf, fischer wf